xdom(f). v=f(x)   P(x;v) == x:A. x  dom(f)  P(x;f(x)) 

latex

---

clarification:

fpf-all(A; eq; f; x,v.P(x;v)) == x:A. fpf-dom(eq; x; f)  P(x;fpf-ap(f; eq; x)) 

latex

Definitions	xdom(f). v=f(x)   P(x;v), x:A. B(x), P  Q, b, x  dom(f), f(x)
FDL editor aliases	fpf-all